<!DOCTYPE html>
<!--
     SPDX-License-Identifier: CC-BY-SA-4.0
     SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
-->
<!-- Page last generated 2025-02-20 03:16:15 +0000 -->
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta http-equiv="X-UA-Compatible" content="IE=edge">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>seL4Test | seL4 docs</title>

    <!-- Our stylesheet and theme stylesheet.  Contains bootstrap. -->
    <link rel="stylesheet" href="/assets/css/style.css" type="text/css">
    <!-- Font awesome -->
    <link href="https://use.fontawesome.com/releases/v5.0.8/css/all.css" rel="stylesheet">
    <link href="https://fonts.googleapis.com/css2?family=Roboto&display=swap" rel="stylesheet">
    <!-- Pygments syntax highlighting  -->
    <link rel="stylesheet" href="/assets/css/highlighting/trac.css" type="text/css">
    <link rel="icon" type="image/x-icon" href="/assets/favicon.ico"><script defer data-domain="docs.sel4.systems"
	    src="https://analytics.sel4.systems/js/script.js"></script></head>

  <body class="container-fluid">

    



<header>
  <ul class="row menu">
    <li class="col-xs-12 col-md-2" >
            <a href="https://sel4.systems" class="skip-icon">
              <img class="img-responsive" src="/assets/logo-text-white.svg" alt="seL4 logo" />
            </a>
    </li>
    <li class="col-xs-12 col-md-10 menu">
      <nav aria-label="Banner links">
        <h2><a href="/Resources" />Resources</h2>
        <h2><a href="/processes" />Contributing</a></h2>
        <h2><a href="/projects" />Projects</h2>
        <h2><a href="/Tutorials" />Tutorials</h2>
        <iframe title="DuckDuckGo search bar" src="https://duckduckgo.com/search.html?site=docs.sel4.systems&prefill=Search%20sel4.systems" style="overflow:hidden;margin-bottom:10px; padding:0;height:40px;float:right;border-width: 0px"></iframe>
      </nav>
    </li>
  </ul>
  <div class="clear"></div>
  
<div class="breadcrumbs bootstrap hidden-sm-down">
  <nav class="sel-breadcrumb" aria-label="Breadcrumb" >
    <ol class=" list-unstyled" vocab="http://schema.org/" typeof="BreadcrumbList">
      
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/">
              <span property="name"><b>seL4 Docs</b></span>
            </a>
            <meta property="position" content="1" />
        </li>
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/projects/">
              <span property="name"><b>Projects</b></span>
            </a>
            <meta property="position" content="2" />
        </li>
      
        

        
          <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <span property="name">seL4Test</span>
            <meta property="position" content="3" /></li>
          
    </ol>
  </nav>
  <nav class="sel-version" aria-label="Current Versions">
    <ol class="list-unstyled">
      <li class="list-unstyled text-right" style="margin-left:auto; padding:0rem 0rem;">
        Current versions:</li>
      <li class="list-unstyled text-right">
      <a href="/releases/sel4/13.0.0"><b>seL4-13.0.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/microkit/1.4.1"><b>microkit-1.4.1</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/camkes/camkes-3.11.0"><b>camkes-3.11.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/capdl/0.3.0"><b>capDL-0.3.0</b></a></li>
      </ol>
  </nav>
  <div class='clear'></div>
</div>


</header>

    <main>
      <div class="row">
  <div class="hidden-xs col-sm-4 col-md-3 col-lg-2">
    


<div class="sidebar">















    <ul class="nav nav-sidebar">
  
    
    

    
        <li class="">
            <a class="" href="/projects/sel4/">seL4</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/l4v/">L4.verified</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/camkes/">CAmkES</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/capdl/">CapDL</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/elfloader/">Elfloader</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/buildsystem/">seL4 Buildsystem</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/user_libs/">user_libs</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/sel4runtime/">The seL4 run-time</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/sel4webserver/">seL4webserver</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/sel4-tutorials/">seL4 tutorials</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/sel4bench/">sel4bench</a>
        </li>
  
    
    

    
        <li class="active">
            <a class="" href="/projects/sel4test/">seL4Test</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/virtualization/">Virtualization</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/camkes-vm/">camkes-vm</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/dockerfiles/">Dockerfiles</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/docsite/">seL4 Documentation website</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/sel4_tools/">seL4_tools</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/microkit/">Microkit</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/hardware_hacks/">Hardware Hacks</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/rust/">Rust</a>
        </li>
  
    </ul>


</div>

  </div>
  <div class="content col-sm-8 col-md-6 col-lg-7 main">
    <h1 id="sel4test">seL4Test</h1>

<p><a href="https://github.com/seL4/sel4test-manifest">sel4test</a> is a test suite for seL4.</p>

<p>First make sure you have
<a href="/HostDependencies#sel4-build-dependencies">set up your machine</a>.</p>

<h2 id="getting-the-code">Getting the Code</h2>

<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="nb">mkdir </span>sel4test
<span class="nb">cd </span>sel4test
repo init <span class="nt">-u</span> https://github.com/seL4/sel4test-manifest.git
repo <span class="nb">sync
ls</span>
<span class="c"># apps/ CMakeLists.txt init-build.sh kernel libs/ projects/ tools/</span>
</code></pre></div></div>

<p>This clones the seL4 kernel, the test suite, some libraries used by the
tests, and some tools used in the build process. By default, the current
master branch of the kernel is cloned. To clone a specific version of
the kernel and compatible libraries and tools, replace the</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>repo init
</code></pre></div></div>
<p>line above with:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>repo init -u https://github.com/seL4/sel4test-manifest.git -b refs/tags/
</code></pre></div></div>

<p>In this example we clone version  of the kernel. For more information on version
numbers, see <a href="/ReleaseProcess#version-numbers">ReleaseProcess</a>.</p>

<h2 id="build-it">Build it</h2>
<h3 id="configuration">Configuration</h3>

<p>The CMake build environment supports a number of platforms. For information regarding our supported hardware platforms and their corresponding CMake
configuration arguments, see the <a href="/Hardware">Supported Platforms</a> page. Platforms that we test and are in-regression are listed as being maintained by the seL4 Foundation.</p>

<p>To start a build with a specific configuration we can create a new subdirectory from the project root
and initialise it with CMake:</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code># create build directory
mkdir build
cd build
# configure build directory
../init-build.sh -DPLATFORM=&lt;platform-name&gt; -DRELEASE=[TRUE|FALSE] -DSIMULATION=[TRUE|FALSE]
</code></pre></div></div>
<p>This configures your build directory with the necessary CMake configuration for your chosen platform.</p>

<p>You can look at and edit the CMake configuration options from your build directory using</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>ccmake .
</code></pre></div></div>

<p>It is also important to note that meta options such as <code class="language-plaintext highlighter-rouge">PLATFORM</code> and <code class="language-plaintext highlighter-rouge">SIMULATION</code> will override various settings in the
seL4test build system in order to maintain the meta configuration. This can however be disabled if you first
enable the <code class="language-plaintext highlighter-rouge">Sel4testAllowSettingsOverride</code> variable.</p>

<h3 id="useful-configuration-options">Useful configuration options</h3>
<p>For an overview of the CMake build system and further configuration options, including configuring for
cross compilation (targeting ARM), see <a href="/Developing/Building/Using">seL4’s CMake Build System</a>.</p>

<h2 id="building">Building</h2>
<p>When you’ve configured the system, you can build it by running:</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>ninja
</code></pre></div></div>

<h2 id="running-it">Running it</h2>

<h3 id="ia32-example">IA32 Example</h3>
<p>We will now build seL4test for ia32, to run on the QEMU simulator.</p>

<p>Passing <code class="language-plaintext highlighter-rouge">-DSIMULATION=TRUE</code> to CMake produces a script to simulate our release ia32 build. The following commands
will configure our CMake build:</p>

<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="nb">mkdir </span>ia32_build
<span class="nb">cd </span>ia32_build
../init-build.sh <span class="nt">-DPLATFORM</span><span class="o">=</span>ia32 <span class="nt">-DRELEASE</span><span class="o">=</span>TRUE <span class="nt">-DSIMULATION</span><span class="o">=</span>TRUE
</code></pre></div></div>

<p>Build it:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>ninja
</code></pre></div></div>

<p>Executing the following commands will run qemu and point it towards the image we just built:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>./simulate
...
ELF-loading userland images from boot modules:
size=0x1dd000 v_entry=0x806716f v_start=0x8048000 v_end=0x8225000 p_start=0x21f000 p_end=0x3fc000
Moving loaded userland images to final location: from=0x21f000 to=0x12e000 size=0x1dd000
Starting node #0 with APIC ID 0
Booting all finished, dropped to user space
...
Starting test 18: BIND0001
Running test BIND0001 (Test that a bound tcb waiting on a sync endpoint receives normal sync ipc and notification notifications.)
Test BIND0001 passed
Starting test 19: BIND0002
Running test BIND0002 (Test that a bound tcb waiting on its bound notification recieves notifications)
Test BIND0002 passed
Starting test 20: BIND0003
Running test BIND0003 (Test IPC ordering 1) bound tcb waits on bound notification 2, true) another tcb sends a message)
Test BIND0003 passed
...
</code></pre></div></div>
<p>To exit qemu, press <code class="language-plaintext highlighter-rouge">Ctrl-a</code>, then <code class="language-plaintext highlighter-rouge">x</code>. The text string<code class="language-plaintext highlighter-rouge"> All is well in the universe</code> indicates a successful build.</p>

<p>We can further configure the test suite build to print out JUnit-style XML. Thus enabling the output to be parsed by various tools.
To do so, edit the build settings through <code class="language-plaintext highlighter-rouge">ccmake</code>, enabling the <code class="language-plaintext highlighter-rouge">Sel4testAllowSettingsOverride</code> and <code class="language-plaintext highlighter-rouge">LibSel4TestPrintXML</code> variables.</p>

<h2 id="testing-a-customised-kernel">Testing a Customised Kernel</h2>

<p>Suppose you’ve got seL4 checked out in <code class="language-plaintext highlighter-rouge">~/projects/seL4</code>, and sel4test in
<code class="language-plaintext highlighter-rouge">~/tests/sel4test</code>, and you have been making changes on a feature branch of seL4 named
<code class="language-plaintext highlighter-rouge">awesome-new-feature</code>. You want to test if your modified kernel
still passes all the tests in sel4test.</p>

<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="nb">cd</span> ~/tests/sel4tests/kernel
git remote add feature ~/projects/seL4
git fetch feature
git checkout feature/awesome-new-feature
<span class="nb">cd</span> ..
</code></pre></div></div>

<p>Now the kernel in sel4test has been changed to your custom kernel.
Now just build and run the test suite as above.</p>

<h2 id="running-a-subset-of-the-tests">Running a subset of the tests</h2>
<p>You can use a regular expression to select a subset of the
tests. This can be configured by setting the CMake variable <code class="language-plaintext highlighter-rouge">LibSel4TestPrinterRegex</code>. We can modify this
variable by running <code class="language-plaintext highlighter-rouge">ccmake .</code> in our build directory. By default the test suite runs all tests.</p>

  </div>







  
    
<div class="sidebar-toc hidden-xs hidden-sm col-md-3 col-lg-3">
    <ul id="toc" class="section-nav">
<li class="toc-entry toc-h2"><a href="#getting-the-code">Getting the Code</a></li>
<li class="toc-entry toc-h2"><a href="#build-it">Build it</a>
<ul>
<li class="toc-entry toc-h3"><a href="#configuration">Configuration</a></li>
<li class="toc-entry toc-h3"><a href="#useful-configuration-options">Useful configuration options</a></li>
</ul>
</li>
<li class="toc-entry toc-h2"><a href="#building">Building</a></li>
<li class="toc-entry toc-h2"><a href="#running-it">Running it</a>
<ul>
<li class="toc-entry toc-h3"><a href="#ia32-example">IA32 Example</a></li>
</ul>
</li>
<li class="toc-entry toc-h2"><a href="#testing-a-customised-kernel">Testing a Customised Kernel</a></li>
<li class="toc-entry toc-h2"><a href="#running-a-subset-of-the-tests">Running a subset of the tests</a></li>
</ul>
</div>

  
  
<div class="sidebar-toc hidden-xs hidden-sm col-md-3 col-lg-3">
  
    <ul class="section-nav">
    	<h2> seL4Test </h2> 
        <li>
          
          <a style=" font-weight: bold; " class="" href="/projects/sel4test/">
            Documentation homepage
          </a>
        </li>








        <li>
          
          <a style="" class="" href="/projects/sel4test/status.html">
            Status
          </a>
        </li>










    
        <h3>Repositories</h3>
    
        <li>
          <a class="" href="https://github.com/sel4/sel4test">
            sel4test
          </a>
        </li>

    
        <li>
          <a class="" href="https://github.com/sel4/sel4test-manifest">
            sel4test-manifest
          </a>
        </li>









  







    
        <h3>Recent Updates</h3>
    
        <li>
          <a style="" href="/updates/sel4test/11.0.x.html">
            seL4 11.0.x-compatible
          </a>
        </li>

    </ul>

</div>


</div>

    </main>
    


<footer class="site-footer">

  <h2 class="footer-heading">seL4 docs</h2>

  <div class="footer-col-wrapper">

    <div class="col-md-2">
      



<ul class="social-media-list">
  <li><a href="https://github.com/sel4"><i class="fab fa-github"></i> <span class="username">sel4</span></a></li><li><a href="https://github.com/sel4proj"><i class="fab fa-github"></i> <span class="username">sel4proj</span></a></li>
</ul>

    </div>

    <div class="col-md-8">
      <ul class="list-unstyled">
        <li>
          This site is for displaying seL4 related documentation.  Pull requests are welcome.
        </li>
        
          <li>
            Site last updated: Fri Feb 7 10:17:38 2025 +1100 ee78c8857c
          </li>
          <li>
                Page last updated: Thu Nov 11 11:50:06 2021 +1100 5fc78c1c47
          </li>
        
      </ul>
    </div>
    <div class="col-md-2">
<a href="https://github.com/seL4/docs/blob/master/projects/sel4test/index.md">View page on GitHub</a>
      <br />
      <a href="https://github.com/seL4/docs/edit/master/projects/sel4test/index.md">Edit page on GitHub</a>
      <br />
      <a href="/sitemap">Sitemap</a>
    </div>

  </div>

</footer>

  </body>
</html>
